|
Logics for computability are formulations of logic which capture some aspect of computability as a basic notion. This usually involves a mix of special logical connectives as well as semantics which explains how the logic is to be interpreted in a computational way. Probably the first formal treatment of logic for computability is the ''realizability interpretation'' by Stephen Kleene in 1945, who gave an interpretation of intuitionistic number theory in terms of Turing machine computations. His motivation was to make precise the ''Heyting-Brouwer-Kolmogorov (BHK) interpretation'' of intuitionism, according to which proofs of mathematical statements are to be viewed as constructive procedures. With the rise of many other kinds of logic, such as modal logic and linear logic, and novel semantic models, such as game semantics, logics for computability have been formulated in several contexts. Here we mention two. ==Modal logic for computability== Kleene's original realizability interpretation has received much attention among those who study connections between computability and logic. It was extended to full higher-order intuitionistic logic by Martin Hyland in 1982 who constructed the effective topos. In 2002, Steven Awodey, Lars Birkedal, and Dana Scott formulated a modal logic for computability which extended the usual realizability interpretation with two modal operators expressing the notion of being "computably true". 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Logics for computability」の詳細全文を読む スポンサード リンク
|